Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar4/CimeSLASHtree.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> GE₂(x, max₁(y))
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)
SIZE₁(n₃(x, y, z)) -> +¹₂(+₂(size₁(x), size₁(y)), 1₁(#))
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> 0¹₁(+₂(+₂(x, y), 1₁(#)))
-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> +¹₂(size₁(x), size₁(y))
BS₁(n₃(x, y, z)) -> BS₁(z)
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(y), size₁(z)))
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(z), size₁(y)))
WB₁(n₃(x, y, z)) -> AND₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))
BS₁(n₃(x, y, z)) -> AND₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
GE₂(0₁(x), 1₁(y)) -> NOT₁(ge₂(y, x))
SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)
WB₁(n₃(x, y, z)) -> SIZE₁(y)
WB₁(n₃(x, y, z)) -> SIZE₁(z)
BS₁(n₃(x, y, z)) -> BS₁(y)
MIN₁(n₃(x, y, z)) -> MIN₁(y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))
WB₁(n₃(x, y, z)) -> AND₂(wb₁(y), wb₁(z))
-¹₂(1₁(x), 1₁(y)) -> 0¹₁(-₂(x, y))
BS₁(n₃(x, y, z)) -> MAX₁(y)
WB₁(n₃(x, y, z)) -> GE₂(size₁(y), size₁(z))
+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> 0¹₁(-₂(x, y))
MAX₁(n₃(x, y, z)) -> MAX₁(z)
WB₁(n₃(x, y, z)) -> -¹₂(size₁(y), size₁(z))
WB₁(n₃(x, y, z)) -> -¹₂(size₁(z), size₁(y))
BS₁(n₃(x, y, z)) -> AND₂(ge₂(x, max₁(y)), ge₂(min₁(z), x))
+¹₂(0₁(x), 0₁(y)) -> 0¹₁(+₂(x, y))
WB₁(n₃(x, y, z)) -> WB₁(z)
GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
WB₁(n₃(x, y, z)) -> WB₁(y)
GE₂(#, 0₁(x)) -> GE₂(#, x)
BS₁(n₃(x, y, z)) -> MIN₁(z)
BS₁(n₃(x, y, z)) -> GE₂(min₁(z), x)
BS₁(n₃(x, y, z)) -> AND₂(bs₁(y), bs₁(z))
WB₁(n₃(x, y, z)) -> IF₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y))))
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> GE₂(x, max₁(y))
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)
SIZE₁(n₃(x, y, z)) -> +¹₂(+₂(size₁(x), size₁(y)), 1₁(#))
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> 0¹₁(+₂(+₂(x, y), 1₁(#)))
-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> +¹₂(size₁(x), size₁(y))
BS₁(n₃(x, y, z)) -> BS₁(z)
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(y), size₁(z)))
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(z), size₁(y)))
WB₁(n₃(x, y, z)) -> AND₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))
BS₁(n₃(x, y, z)) -> AND₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
GE₂(0₁(x), 1₁(y)) -> NOT₁(ge₂(y, x))
SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)
WB₁(n₃(x, y, z)) -> SIZE₁(y)
WB₁(n₃(x, y, z)) -> SIZE₁(z)
BS₁(n₃(x, y, z)) -> BS₁(y)
MIN₁(n₃(x, y, z)) -> MIN₁(y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))
WB₁(n₃(x, y, z)) -> AND₂(wb₁(y), wb₁(z))
-¹₂(1₁(x), 1₁(y)) -> 0¹₁(-₂(x, y))
BS₁(n₃(x, y, z)) -> MAX₁(y)
WB₁(n₃(x, y, z)) -> GE₂(size₁(y), size₁(z))
+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> 0¹₁(-₂(x, y))
MAX₁(n₃(x, y, z)) -> MAX₁(z)
WB₁(n₃(x, y, z)) -> -¹₂(size₁(y), size₁(z))
WB₁(n₃(x, y, z)) -> -¹₂(size₁(z), size₁(y))
BS₁(n₃(x, y, z)) -> AND₂(ge₂(x, max₁(y)), ge₂(min₁(z), x))
+¹₂(0₁(x), 0₁(y)) -> 0¹₁(+₂(x, y))
WB₁(n₃(x, y, z)) -> WB₁(z)
GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
WB₁(n₃(x, y, z)) -> WB₁(y)
GE₂(#, 0₁(x)) -> GE₂(#, x)
BS₁(n₃(x, y, z)) -> MIN₁(z)
BS₁(n₃(x, y, z)) -> GE₂(min₁(z), x)
BS₁(n₃(x, y, z)) -> AND₂(bs₁(y), bs₁(z))
WB₁(n₃(x, y, z)) -> IF₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y))))
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 9 SCCs with 24 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAX₁(n₃(x, y, z)) -> MAX₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

MAX₁(n₃(x, y, z)) -> MAX₁(z)

Used argument filtering: MAX₁(x1) = x1
n₃(x1, x2, x3) = n₁(x3)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MIN₁(n₃(x, y, z)) -> MIN₁(y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

MIN₁(n₃(x, y, z)) -> MIN₁(y)

Used argument filtering: MIN₁(x1) = x1
n₃(x1, x2, x3) = n₁(x2)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(#, 0₁(x)) -> GE₂(#, x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

GE₂(#, 0₁(x)) -> GE₂(#, x)

Used argument filtering: GE₂(x1, x2) = x2
0₁(x1) = 0₁(x1)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> BS₁(y)
BS₁(n₃(x, y, z)) -> BS₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

BS₁(n₃(x, y, z)) -> BS₁(y)
BS₁(n₃(x, y, z)) -> BS₁(z)

Used argument filtering: BS₁(x1) = x1
n₃(x1, x2, x3) = n₂(x2, x3)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

Used argument filtering: -¹₂(x1, x2) = x2
0₁(x1) = x1
1₁(x1) = 1₁(x1)
# = #
Used ordering: Quasi Precedence: 1_1 > #

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ DependencyGraphProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 2 SCCs.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ AND

                    ↳ QDP

                      ↳ QDPAfsSolverProof

                    ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))

Used argument filtering: -¹₂(x1, x2) = x1
0₁(x1) = 0₁(x1)
-₂(x1, x2) = x1
# = #
1₁(x1) = 1₁(x1)
Used ordering: Quasi Precedence: [0_1, 1_1]

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ AND

                    ↳ QDP

                      ↳ QDPAfsSolverProof

                        ↳ QDP

                          ↳ PisEmptyProof

                    ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ AND

                    ↳ QDP

                    ↳ QDP

                      ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)

Used argument filtering: -¹₂(x1, x2) = x2
0₁(x1) = 0₁(x1)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ AND

                    ↳ QDP

                    ↳ QDP

                      ↳ QDPAfsSolverProof

                        ↳ QDP

                          ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

Used argument filtering: +¹₂(x1, x2) = x2
0₁(x1) = x1
1₁(x1) = x1
+₂(x1, x2) = +₂(x1, x2)
# = #
Used ordering: Quasi Precedence: +_2 > #

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)

Used argument filtering: +¹₂(x1, x2) = x2
0₁(x1) = x1
1₁(x1) = 1₁(x1)
# = #
Used ordering: Quasi Precedence: 1_1 > #

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ QDPAfsSolverProof

                  ↳ QDP

                    ↳ DependencyGraphProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 2 SCCs.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ QDPAfsSolverProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ QDPAfsSolverProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)

Used argument filtering: +¹₂(x1, x2) = x2
0₁(x1) = 0₁(x1)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ QDPAfsSolverProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ QDPAfsSolverProof

                            ↳ QDP

                              ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)

Used argument filtering: SIZE₁(x1) = x1
n₃(x1, x2, x3) = n₂(x1, x2)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

WB₁(n₃(x, y, z)) -> WB₁(y)
WB₁(n₃(x, y, z)) -> WB₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

WB₁(n₃(x, y, z)) -> WB₁(y)
WB₁(n₃(x, y, z)) -> WB₁(z)

Used argument filtering: WB₁(x1) = x1
n₃(x1, x2, x3) = n₂(x2, x3)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.